\begin{tabbing}
generic\=\{i:l\}\+
\\[0ex]($T$; $f$.$S$($f$))
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$R$:($\mathbb{N}\rightarrow$($T$ List)$\rightarrow$Prop$_{\mbox{\scriptsize i}}$).\+
\\[0ex]($\forall$$i$:$\mathbb{N}$, $s$:$T$ List. $\exists$${\it s'}$:$T$ List. $s$ $\leq$ ${\it s'}$ $\in$ $T$ List \& $R$($i$,${\it s'}$))
\\[0ex]\& ($\forall$$f$:($\mathbb{N}\rightarrow$$T$). ($\forall$$i$:$\mathbb{N}$. $\exists$$s$:$T$ List. $R$($i$,$s$) \& ($\forall$$n$:\{0..$\parallel$$s$$\parallel^{-}$\}. $s$[$n$] $=$ $f$($n$) $\in$ $T$)) $\Rightarrow$ $S$($f$))
\-
\end{tabbing}